Analysis of recursive programs in the presence of concurrency andshared memory is undecidable. A common approach is to removethe recursive nature of the program while dealing with concurrency.A different approach is to bound the number of context switches,which has been shown to be very useful for program analysis.In previous work, Qadeer and Rehof [36] showed that context-boundedanalysis is decidable for recursive programs under a finite-stateabstraction of program data. In this paper, we generalize theirresult to infinite-state abstractions, and also provide a new symbolicalgorithm for the finite case.
展开▼
